<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Types: Type Systems</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Types<span class="subtitle">Type Systems</span></h1>

<div class="code">
</div>

<div class="doc">

<div class="paragraph"> </div>

 Our next major topic is <i>type systems</i> -- static program
    analyses that classify expressions according to the "shapes" of
    their results.  We'll begin with a typed version of the simplest
    imaginable language, to introduce the basic ideas of types and
    typing rules and the fundamental theorems about type systems:
    <i>type preservation</i> and <i>progress</i>.  In chapter <a href="Stlc.html"><span class="inlineref">Stlc</span></a> we'll move
    on to the <i>simply typed lambda-calculus</i>, which lives at the core
    of every modern functional programming language (including
    Coq!). 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.Arith.html#"><span class="id" title="library">Arith.Arith</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Imp</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Types.html#multi"><span class="id" title="inductive">multi</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab187"></a><h1 class="section">Typed Arithmetic Expressions</h1>

<div class="paragraph"> </div>

 To motivate the discussion of type systems, let's begin as
    usual with a tiny toy language.  We want it to have the potential
    for programs to go wrong because of runtime type errors, so we
    need something a tiny bit more complex than the language of
    constants and addition that we used in chapter <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a>: a
    single kind of data (e.g., numbers) is too simple, but just two
    kinds (numbers and booleans) gives us enough material to tell an
    interesting story.

<div class="paragraph"> </div>

    The language definition is completely routine. 
</div>

<div class="doc">
<a id="lab188"></a><h2 class="section">Syntax</h2>

<div class="paragraph"> </div>

 Here is the syntax, informally:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" title="var">tru</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">fls</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">test</span> <span class="id" title="var">t</span> <span class="id" title="keyword">then</span> <span class="id" title="var">t</span> <span class="id" title="keyword">else</span> <span class="id" title="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">zro</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">scc</span> <span class="id" title="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">prd</span> <span class="id" title="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">iszro</span> <span class="id" title="var">t</span>
<div class="paragraph"> </div>

</span>    And here it is formally: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="tm" class="idref" href="#tm"><span class="id" title="inductive">tm</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="tru" class="idref" href="#tru"><span class="id" title="constructor">tru</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="fls" class="idref" href="#fls"><span class="id" title="constructor">fls</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="test" class="idref" href="#test"><span class="id" title="constructor">test</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="zro" class="idref" href="#zro"><span class="id" title="constructor">zro</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="scc" class="idref" href="#scc"><span class="id" title="constructor">scc</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="prd" class="idref" href="#prd"><span class="id" title="constructor">prd</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="iszro" class="idref" href="#iszro"><span class="id" title="constructor">iszro</span></a> : <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm:1"><span class="id" title="inductive">tm</span></a>.<br/>
</div>

<div class="doc">
<i>Values</i> are <span class="inlinecode"><span class="id" title="var">tru</span></span>, <span class="inlinecode"><span class="id" title="var">fls</span></span>, and numeric values... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="bvalue" class="idref" href="#bvalue"><span class="id" title="inductive">bvalue</span></a> : <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="bv_tru" class="idref" href="#bv_tru"><span class="id" title="constructor">bv_tru</span></a> : <a class="idref" href="Types.html#bvalue:3"><span class="id" title="inductive">bvalue</span></a> <a class="idref" href="Types.html#tru"><span class="id" title="constructor">tru</span></a><br/>
&nbsp;&nbsp;| <a id="bv_fls" class="idref" href="#bv_fls"><span class="id" title="constructor">bv_fls</span></a> : <a class="idref" href="Types.html#bvalue:3"><span class="id" title="inductive">bvalue</span></a> <a class="idref" href="Types.html#fls"><span class="id" title="constructor">fls</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="nvalue" class="idref" href="#nvalue"><span class="id" title="inductive">nvalue</span></a> : <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="nv_zro" class="idref" href="#nv_zro"><span class="id" title="constructor">nv_zro</span></a> : <a class="idref" href="Types.html#nvalue:5"><span class="id" title="inductive">nvalue</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a><br/>
&nbsp;&nbsp;| <a id="nv_scc" class="idref" href="#nv_scc"><span class="id" title="constructor">nv_scc</span></a> : <span class="id" title="keyword">∀</span> <a id="t:7" class="idref" href="#t:7"><span class="id" title="binder">t</span></a>, <a class="idref" href="Types.html#nvalue:5"><span class="id" title="inductive">nvalue</span></a> <a class="idref" href="Types.html#t:7"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#nvalue:5"><span class="id" title="inductive">nvalue</span></a> (<a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#t:7"><span class="id" title="variable">t</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="value" class="idref" href="#value"><span class="id" title="definition">value</span></a> (<a id="t:8" class="idref" href="#t:8"><span class="id" title="binder">t</span></a> : <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a>) := <a class="idref" href="Types.html#bvalue"><span class="id" title="inductive">bvalue</span></a> <a class="idref" href="Types.html#t:8"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="Types.html#nvalue"><span class="id" title="inductive">nvalue</span></a> <a class="idref" href="Types.html#t:8"><span class="id" title="variable">t</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Types.html#bvalue"><span class="id" title="inductive">bvalue</span></a> <a class="idref" href="Types.html#nvalue"><span class="id" title="inductive">nvalue</span></a> : <span class="id" title="var">core</span>.<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="Types.html#value"><span class="id" title="definition">value</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab189"></a><h2 class="section">Operational Semantics</h2>

<div class="paragraph"> </div>

 Here is the single-step relation, first informally... 
<div class="paragraph"> </div>

<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_TestTru) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">test tru then t<sub>1</sub> else t<sub>2</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_TestFls) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">test fls then t<sub>1</sub> else t<sub>2</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Test) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">test t<sub>1</sub> then t<sub>2</sub> else t<sub>3</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> test t<sub>1</sub>' then t<sub>2</sub> else t<sub>3</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Scc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">scc t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> scc t<sub>1</sub>'</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_PrdZro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">prd zro <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> zro</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">numeric value v</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_PrdScc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">prd (scc v) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> v</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Prd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">prd t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> prd t<sub>1</sub>'</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_IszroZro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">iszro zro <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> tru</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">numeric value v</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_IszroScc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">iszro (scc v) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> fls</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Iszro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">iszro t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> iszro t<sub>1</sub>'</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 ... and then formally: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Reserved Notation</span> &quot;t '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t'" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="step" class="idref" href="#step"><span class="id" title="inductive">step</span></a> : <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="ST_TestTru" class="idref" href="#ST_TestTru"><span class="id" title="constructor">ST_TestTru</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:11" class="idref" href="#t<sub>1</sub>:11"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:12" class="idref" href="#t<sub>2</sub>:12"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#tru"><span class="id" title="constructor">tru</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:11"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#t<sub>2</sub>:12"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t<sub>1</sub>:11"><span class="id" title="variable">t<sub>1</sub></span></a><br/>
&nbsp;&nbsp;| <a id="ST_TestFls" class="idref" href="#ST_TestFls"><span class="id" title="constructor">ST_TestFls</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:13" class="idref" href="#t<sub>1</sub>:13"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:14" class="idref" href="#t<sub>2</sub>:14"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#fls"><span class="id" title="constructor">fls</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:13"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#t<sub>2</sub>:14"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t<sub>2</sub>:14"><span class="id" title="variable">t<sub>2</sub></span></a><br/>
&nbsp;&nbsp;| <a id="ST_Test" class="idref" href="#ST_Test"><span class="id" title="constructor">ST_Test</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:15" class="idref" href="#t<sub>1</sub>:15"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':16" class="idref" href="#t<sub>1</sub>':16"><span class="id" title="binder">t<sub>1</sub>'</span></a> <a id="t<sub>2</sub>:17" class="idref" href="#t<sub>2</sub>:17"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:18" class="idref" href="#t<sub>3</sub>:18"><span class="id" title="binder">t<sub>3</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#t<sub>1</sub>:15"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t<sub>1</sub>':16"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:15"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#t<sub>2</sub>:17"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Types.html#t<sub>3</sub>:18"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#t<sub>1</sub>':16"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="Types.html#t<sub>2</sub>:17"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Types.html#t<sub>3</sub>:18"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a id="ST_Scc" class="idref" href="#ST_Scc"><span class="id" title="constructor">ST_Scc</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:19" class="idref" href="#t<sub>1</sub>:19"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':20" class="idref" href="#t<sub>1</sub>':20"><span class="id" title="binder">t<sub>1</sub>'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#t<sub>1</sub>:19"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t<sub>1</sub>':20"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:19"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#t<sub>1</sub>':20"><span class="id" title="variable">t<sub>1</sub>'</span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a id="ST_PrdZro" class="idref" href="#ST_PrdZro"><span class="id" title="constructor">ST_PrdZro</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#prd"><span class="id" title="constructor">prd</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a><br/>
&nbsp;&nbsp;| <a id="ST_PrdScc" class="idref" href="#ST_PrdScc"><span class="id" title="constructor">ST_PrdScc</span></a> : <span class="id" title="keyword">∀</span> <a id="v:21" class="idref" href="#v:21"><span class="id" title="binder">v</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#nvalue"><span class="id" title="inductive">nvalue</span></a> <a class="idref" href="Types.html#v:21"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#prd"><span class="id" title="constructor">prd</span></a> (<a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#v:21"><span class="id" title="variable">v</span></a>)<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#v:21"><span class="id" title="variable">v</span></a><br/>
&nbsp;&nbsp;| <a id="ST_Prd" class="idref" href="#ST_Prd"><span class="id" title="constructor">ST_Prd</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:22" class="idref" href="#t<sub>1</sub>:22"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':23" class="idref" href="#t<sub>1</sub>':23"><span class="id" title="binder">t<sub>1</sub>'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#t<sub>1</sub>:22"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t<sub>1</sub>':23"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#prd"><span class="id" title="constructor">prd</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:22"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#prd"><span class="id" title="constructor">prd</span></a> <a class="idref" href="Types.html#t<sub>1</sub>':23"><span class="id" title="variable">t<sub>1</sub>'</span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a id="ST_IszroZro" class="idref" href="#ST_IszroZro"><span class="id" title="constructor">ST_IszroZro</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#iszro"><span class="id" title="constructor">iszro</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#tru"><span class="id" title="constructor">tru</span></a><br/>
&nbsp;&nbsp;| <a id="ST_IszroScc" class="idref" href="#ST_IszroScc"><span class="id" title="constructor">ST_IszroScc</span></a> : <span class="id" title="keyword">∀</span> <a id="v:24" class="idref" href="#v:24"><span class="id" title="binder">v</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#nvalue"><span class="id" title="inductive">nvalue</span></a> <a class="idref" href="Types.html#v:24"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#iszro"><span class="id" title="constructor">iszro</span></a> (<a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#v:24"><span class="id" title="variable">v</span></a>)<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#fls"><span class="id" title="constructor">fls</span></a><br/>
&nbsp;&nbsp;| <a id="ST_Iszro" class="idref" href="#ST_Iszro"><span class="id" title="constructor">ST_Iszro</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:25" class="idref" href="#t<sub>1</sub>:25"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':26" class="idref" href="#t<sub>1</sub>':26"><span class="id" title="binder">t<sub>1</sub>'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#t<sub>1</sub>:25"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t<sub>1</sub>':26"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#iszro"><span class="id" title="constructor">iszro</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:25"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Types.html#iszro"><span class="id" title="constructor">iszro</span></a> <a class="idref" href="Types.html#t<sub>1</sub>':26"><span class="id" title="variable">t<sub>1</sub>'</span></a><a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation">)</span></a><br/>
<br/>
<span class="id" title="keyword">where</span> <a id=":::x_'--&gt;'_x" class="idref" href="#:::x_'--&gt;'_x"><span class="id" title="notation">&quot;</span></a>t '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t'" := (<a class="idref" href="Types.html#step:10"><span class="id" title="inductive">step</span></a> <span class="id" title="var">t</span> <span class="id" title="var">t'</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Types.html#step"><span class="id" title="inductive">step</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
Notice that the <span class="inlinecode"><span class="id" title="var">step</span></span> relation doesn't care about whether the
    expression being stepped makes global sense -- it just checks that
    the operation in the <i>next</i> reduction step is being applied to the
    right kinds of operands.  For example, the term <span class="inlinecode"><span class="id" title="var">scc</span></span> <span class="inlinecode"><span class="id" title="var">tru</span></span> cannot
    take a step, but the almost as obviously nonsensical term
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">scc</span> (<span class="id" title="var">test</span> <span class="id" title="var">tru</span> <span class="id" title="keyword">then</span> <span class="id" title="var">tru</span> <span class="id" title="keyword">else</span> <span class="id" title="var">tru</span>)
<div class="paragraph"> </div>

</span>    can take a step (once, before becoming stuck). 
</div>

<div class="doc">
<a id="lab190"></a><h2 class="section">Normal Forms and Values</h2>

<div class="paragraph"> </div>

 The first interesting thing to notice about this <span class="inlinecode"><span class="id" title="var">step</span></span> relation
    is that the strong progress theorem from the <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a> chapter
    fails here.  That is, there are terms that are normal forms (they
    can't take a step) but not values (because we have not included
    them in our definition of possible "results of reduction").  Such
    terms are <i>stuck</i>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Notation</span> <a id="step_normal_form" class="idref" href="#step_normal_form"><span class="id" title="abbreviation">step_normal_form</span></a> := (<a class="idref" href="Smallstep.html#normal_form"><span class="id" title="definition">normal_form</span></a> <a class="idref" href="Types.html#step"><span class="id" title="inductive">step</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="stuck" class="idref" href="#stuck"><span class="id" title="definition">stuck</span></a> (<a id="t:27" class="idref" href="#t:27"><span class="id" title="binder">t</span></a> : <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#step_normal_form"><span class="id" title="abbreviation">step_normal_form</span></a> <a class="idref" href="Types.html#t:27"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="Types.html#value"><span class="id" title="definition">value</span></a> <a class="idref" href="Types.html#t:27"><span class="id" title="variable">t</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="Types.html#stuck"><span class="id" title="definition">stuck</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab191"></a><h4 class="section">Exercise: 2 stars, standard (some_term_is_stuck)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Example</span> <a id="some_term_is_stuck" class="idref" href="#some_term_is_stuck"><span class="id" title="definition">some_term_is_stuck</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="t:28" class="idref" href="#t:28"><span class="id" title="binder">t</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Types.html#stuck"><span class="id" title="definition">stuck</span></a> <a class="idref" href="Types.html#t:28"><span class="id" title="variable">t</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 However, although values and normal forms are <i>not</i> the same in
    this language, the set of values is a subset of the set of normal
    forms.  This is important because it shows we did not accidentally
    define things so that some value could still take a step. 
<div class="paragraph"> </div>

<a id="lab192"></a><h4 class="section">Exercise: 3 stars, standard (value_is_nf)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="value_is_nf" class="idref" href="#value_is_nf"><span class="id" title="lemma">value_is_nf</span></a> : <span class="id" title="keyword">∀</span> <a id="t:29" class="idref" href="#t:29"><span class="id" title="binder">t</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#value"><span class="id" title="definition">value</span></a> <a class="idref" href="Types.html#t:29"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#step_normal_form"><span class="id" title="abbreviation">step_normal_form</span></a> <a class="idref" href="Types.html#t:29"><span class="id" title="variable">t</span></a>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>
</div>

<div class="doc">
(Hint: You will reach a point in this proof where you need to
    use an induction to reason about a term that is known to be a
    numeric value.  This induction can be performed either over the
    term itself or over the evidence that it is a numeric value.  The
    proof goes through in either case, but you will find that one way
    is quite a bit shorter than the other.  For the sake of the
    exercise, try to complete the proof both ways.)  <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab193"></a><h4 class="section">Exercise: 3 stars, standard, optional (step_deterministic)</h4>
 Use <span class="inlinecode"><span class="id" title="var">value_is_nf</span></span> to show that the <span class="inlinecode"><span class="id" title="var">step</span></span> relation is also
    deterministic. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="step_deterministic" class="idref" href="#step_deterministic"><span class="id" title="lemma">step_deterministic</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Smallstep.html#deterministic"><span class="id" title="definition">deterministic</span></a> <a class="idref" href="Types.html#step"><span class="id" title="inductive">step</span></a>.<br/>
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab194"></a><h2 class="section">Typing</h2>

<div class="paragraph"> </div>

 The next critical observation is that, although this
    language has stuck terms, they are always nonsensical, mixing
    booleans and numbers in a way that we don't even <i>want</i> to have a
    meaning.  We can easily exclude such ill-typed terms by defining a
    <i>typing relation</i> that relates terms to the types (either numeric
    or boolean) of their final results.  
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="ty" class="idref" href="#ty"><span class="id" title="inductive">ty</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="Bool" class="idref" href="#Bool"><span class="id" title="constructor">Bool</span></a> : <a class="idref" href="Types.html#ty:30"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="Nat" class="idref" href="#Nat"><span class="id" title="constructor">Nat</span></a> : <a class="idref" href="Types.html#ty:30"><span class="id" title="inductive">ty</span></a>.<br/>
</div>

<div class="doc">
In informal notation, the typing relation is often written
    <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> and pronounced "<span class="inlinecode"><span class="id" title="var">t</span></span> has type <span class="inlinecode"><span class="id" title="var">T</span></span>."  The <span class="inlinecode">&#x22A2;</span> symbol
    is called a "turnstile."  Below, we're going to see richer typing
    relations where one or more additional "context" arguments are
    written to the left of the turnstile.  For the moment, the context
    is always empty.  <center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Tru) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; tru &#x2208; Bool</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Fls) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; fls &#x2208; Bool</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; t<sub>1</sub> &#x2208; Bool&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; t<sub>2</sub> &#x2208; T&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; t<sub>3</sub> &#x2208; T</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Test) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; test t<sub>1</sub> then t<sub>2</sub> else t<sub>3</sub> &#x2208; T</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Zro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; zro &#x2208; Nat</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; t<sub>1</sub> &#x2208; Nat</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Scc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; scc t<sub>1</sub> &#x2208; Nat</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; t<sub>1</sub> &#x2208; Nat</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Prd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; prd t<sub>1</sub> &#x2208; Nat</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; t<sub>1</sub> &#x2208; Nat</td>
  <td class="infrulenamecol" rowspan="3">
    (T_IsZro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2; iszro t<sub>1</sub> &#x2208; Bool</td>
  <td></td>
</td>
</table></center>
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Reserved Notation</span> &quot;'&#x22A2;' t '&#x2208;' T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="has_type" class="idref" href="#has_type"><span class="id" title="inductive">has_type</span></a> : <a class="idref" href="Types.html#tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="T_Tru" class="idref" href="#T_Tru"><span class="id" title="constructor">T_Tru</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#tru"><span class="id" title="constructor">tru</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Bool"><span class="id" title="constructor">Bool</span></a><br/>
&nbsp;&nbsp;| <a id="T_Fls" class="idref" href="#T_Fls"><span class="id" title="constructor">T_Fls</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#fls"><span class="id" title="constructor">fls</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Bool"><span class="id" title="constructor">Bool</span></a><br/>
&nbsp;&nbsp;| <a id="T_Test" class="idref" href="#T_Test"><span class="id" title="constructor">T_Test</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:34" class="idref" href="#t<sub>1</sub>:34"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:35" class="idref" href="#t<sub>2</sub>:35"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:36" class="idref" href="#t<sub>3</sub>:36"><span class="id" title="binder">t<sub>3</sub></span></a> <a id="T:37" class="idref" href="#T:37"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:34"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Bool"><span class="id" title="constructor">Bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t<sub>2</sub>:35"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:37"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t<sub>3</sub>:36"><span class="id" title="variable">t<sub>3</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:37"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:34"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#t<sub>2</sub>:35"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Types.html#t<sub>3</sub>:36"><span class="id" title="variable">t<sub>3</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:37"><span class="id" title="variable">T</span></a><br/>
&nbsp;&nbsp;| <a id="T_Zro" class="idref" href="#T_Zro"><span class="id" title="constructor">T_Zro</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a><br/>
&nbsp;&nbsp;| <a id="T_Scc" class="idref" href="#T_Scc"><span class="id" title="constructor">T_Scc</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:38" class="idref" href="#t<sub>1</sub>:38"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:38"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:38"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a><br/>
&nbsp;&nbsp;| <a id="T_Prd" class="idref" href="#T_Prd"><span class="id" title="constructor">T_Prd</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:39" class="idref" href="#t<sub>1</sub>:39"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:39"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#prd"><span class="id" title="constructor">prd</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:39"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a><br/>
&nbsp;&nbsp;| <a id="T_Iszro" class="idref" href="#T_Iszro"><span class="id" title="constructor">T_Iszro</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:40" class="idref" href="#t<sub>1</sub>:40"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:40"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#iszro"><span class="id" title="constructor">iszro</span></a> <a class="idref" href="Types.html#t<sub>1</sub>:40"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Bool"><span class="id" title="constructor">Bool</span></a><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="46525c5c9c73f3cc121f6ba0c58fa00e" class="idref" href="#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&quot;</span></a>'&#x22A2;' t '&#x2208;' T" := (<a class="idref" href="Types.html#has_type:33"><span class="id" title="inductive">has_type</span></a> <span class="id" title="var">t</span> <span class="id" title="var">T</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Types.html#has_type"><span class="id" title="inductive">has_type</span></a> : <span class="id" title="var">core</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="has_type_1" class="idref" href="#has_type_1"><span class="id" title="definition">has_type_1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#fls"><span class="id" title="constructor">fls</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a> (<a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a>) <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#T_Test"><span class="id" title="constructor">T_Test</span></a>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#T_Fls"><span class="id" title="constructor">T_Fls</span></a>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#T_Zro"><span class="id" title="constructor">T_Zro</span></a>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#T_Scc"><span class="id" title="constructor">T_Scc</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#T_Zro"><span class="id" title="constructor">T_Zro</span></a>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
(Since we've included all the constructors of the typing relation
    in the hint database, the <span class="inlinecode"><span class="id" title="tactic">auto</span></span> tactic can actually find this
    proof automatically.) 
<div class="paragraph"> </div>

 It's important to realize that the typing relation is a
    <i>conservative</i> (or <i>static</i>) approximation: it does not consider
    what happens when the term is reduced -- in particular, it does
    not calculate the type of its normal form. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="has_type_not" class="idref" href="#has_type_not"><span class="id" title="definition">has_type_not</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">(</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <a class="idref" href="Types.html#fls"><span class="id" title="constructor">fls</span></a> <a class="idref" href="Types.html#zro"><span class="id" title="constructor">zro</span></a> <a class="idref" href="Types.html#tru"><span class="id" title="constructor">tru</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Bool"><span class="id" title="constructor">Bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Contra</span>. <span class="id" title="var">solve_by_inverts</span> 2. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab195"></a><h4 class="section">Exercise: 1 star, standard, optional (scc_hastype_nat__hastype_nat)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Example</span> <a id="scc_hastype_nat__hastype_nat" class="idref" href="#scc_hastype_nat__hastype_nat"><span class="id" title="definition">scc_hastype_nat__hastype_nat</span></a> : <span class="id" title="keyword">∀</span> <a id="t:41" class="idref" href="#t:41"><span class="id" title="binder">t</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#scc"><span class="id" title="constructor">scc</span></a> <a class="idref" href="Types.html#t:41"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:41"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab196"></a><h3 class="section">Canonical forms</h3>

<div class="paragraph"> </div>

 The following two lemmas capture the fundamental property that the
    definitions of boolean and numeric values agree with the typing
    relation. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="bool_canonical" class="idref" href="#bool_canonical"><span class="id" title="lemma">bool_canonical</span></a> : <span class="id" title="keyword">∀</span> <a id="t:42" class="idref" href="#t:42"><span class="id" title="binder">t</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:42"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Bool"><span class="id" title="constructor">Bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#value"><span class="id" title="definition">value</span></a> <a class="idref" href="Types.html#t:42"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#bvalue"><span class="id" title="inductive">bvalue</span></a> <a class="idref" href="Types.html#t:42"><span class="id" title="variable">t</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">HT</span> [<span class="id" title="var">Hb</span> | <span class="id" title="var">Hn</span>].<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">destruct</span> <span class="id" title="var">Hn</span> <span class="id" title="keyword">as</span> [ | <span class="id" title="var">Hs</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" title="tactic">inversion</span> <span class="id" title="var">HT</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" title="tactic">inversion</span> <span class="id" title="var">HT</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Lemma</span> <a id="nat_canonical" class="idref" href="#nat_canonical"><span class="id" title="lemma">nat_canonical</span></a> : <span class="id" title="keyword">∀</span> <a id="t:43" class="idref" href="#t:43"><span class="id" title="binder">t</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:43"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#Nat"><span class="id" title="constructor">Nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#value"><span class="id" title="definition">value</span></a> <a class="idref" href="Types.html#t:43"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Types.html#nvalue"><span class="id" title="inductive">nvalue</span></a> <a class="idref" href="Types.html#t:43"><span class="id" title="variable">t</span></a>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">HT</span> [<span class="id" title="var">Hb</span> | <span class="id" title="var">Hn</span>].<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hb</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">HT</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">assumption</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab197"></a><h2 class="section">Progress</h2>

<div class="paragraph"> </div>

 The typing relation enjoys two critical properties.  The first is
    that well-typed normal forms are not stuck -- or conversely, if a
    term is well typed, then either it is a value or it can take at
    least one step.  We call this <i>progress</i>. 
<div class="paragraph"> </div>

<a id="lab198"></a><h4 class="section">Exercise: 3 stars, standard (finish_progress)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="progress" class="idref" href="#progress"><span class="id" title="lemma">progress</span></a> : <span class="id" title="keyword">∀</span> <a id="t:44" class="idref" href="#t:44"><span class="id" title="binder">t</span></a> <a id="T:45" class="idref" href="#T:45"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:44"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:45"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#value"><span class="id" title="definition">value</span></a> <a class="idref" href="Types.html#t:44"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="t':46" class="idref" href="#t':46"><span class="id" title="binder">t'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Types.html#t:44"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t':46"><span class="id" title="variable">t'</span></a>.<br/>
</div>

<div class="doc">
Complete the formal proof of the <span class="inlinecode"><span class="id" title="tactic">progress</span></span> property.  (Make sure
    you understand the parts we've given of the informal proof in the
    following exercise before starting -- this will save you a lot of
    time.) 
</div>
<div class="code">
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">HT</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">HT</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;cases&nbsp;that&nbsp;were&nbsp;obviously&nbsp;values,&nbsp;like&nbsp;T_Tru&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;T_Fls,&nbsp;were&nbsp;eliminated&nbsp;immediately&nbsp;by&nbsp;auto&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHT1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> (<a class="idref" href="Types.html#bool_canonical"><span class="id" title="lemma">bool_canonical</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">HT<sub>1</sub></span>) <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="id" title="tactic">∃</span> <span class="id" title="var">t<sub>2</sub></span>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="id" title="tactic">∃</span> <span class="id" title="var">t<sub>3</sub></span>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;can&nbsp;take&nbsp;a&nbsp;step&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">H<sub>1</sub></span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> (<a class="idref" href="Types.html#test"><span class="id" title="constructor">test</span></a> <span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">t<sub>3</sub></span>). <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab199"></a><h4 class="section">Exercise: 3 stars, advanced (finish_progress_informal)</h4>
 Complete the corresponding informal proof: 
<div class="paragraph"> </div>

 <i>Theorem</i>: If <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, then either <span class="inlinecode"><span class="id" title="var">t</span></span> is a value or else
    <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span> for some <span class="inlinecode"><span class="id" title="var">t'</span></span>. 
<div class="paragraph"> </div>

 <i>Proof</i>: By induction on a derivation of <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule in the derivation is <span class="inlinecode"><span class="id" title="var">T_Test</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">test</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>
      <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>, with <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span>, <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>
      <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.  By the IH, either <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is a value or else <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> can step
      to some <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> is a value, then by the canonical forms lemmas
        and the fact that <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span> we have that <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>
        is a <span class="inlinecode"><span class="id" title="var">bvalue</span></span> -- i.e., it is either <span class="inlinecode"><span class="id" title="var">tru</span></span> or <span class="inlinecode"><span class="id" title="var">fls</span></span>.
        If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">tru</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> steps to <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" title="var">ST_TestTru</span></span>,
        while if <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">fls</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> steps to <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span> by
        <span class="inlinecode"><span class="id" title="var">ST_TestFls</span></span>.  Either way, <span class="inlinecode"><span class="id" title="var">t</span></span> can step, which is what
        we wanted to show.

<div class="paragraph"> </div>


</li>
<li> If <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> itself can take a step, then, by <span class="inlinecode"><span class="id" title="var">ST_Test</span></span>, so can
        <span class="inlinecode"><span class="id" title="var">t</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</li>
</ul>
 
</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_finish_progress_informal" class="idref" href="#manual_grade_for_finish_progress_informal"><span class="id" title="definition">manual_grade_for_finish_progress_informal</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 This theorem is more interesting than the strong progress theorem
    that we saw in the <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a> chapter, where <i>all</i> normal forms
    were values.  Here a term can be stuck, but only if it is ill
    typed. 
</div>

<div class="doc">
<a id="lab200"></a><h2 class="section">Type Preservation</h2>

<div class="paragraph"> </div>

 The second critical property of typing is that, when a well-typed
    term takes a step, the result is also a well-typed term. 
<div class="paragraph"> </div>

<a id="lab201"></a><h4 class="section">Exercise: 2 stars, standard (finish_preservation)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="preservation" class="idref" href="#preservation"><span class="id" title="lemma">preservation</span></a> : <span class="id" title="keyword">∀</span> <a id="t:47" class="idref" href="#t:47"><span class="id" title="binder">t</span></a> <a id="t':48" class="idref" href="#t':48"><span class="id" title="binder">t'</span></a> <a id="T:49" class="idref" href="#T:49"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:47"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:49"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#t:47"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t':48"><span class="id" title="variable">t'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t':48"><span class="id" title="variable">t'</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:49"><span class="id" title="variable">T</span></a>.<br/>
</div>

<div class="doc">
Complete the formal proof of the <span class="inlinecode"><span class="id" title="var">preservation</span></span> property.  (Again,
    make sure you understand the informal proof fragment in the
    following exercise first.) 
</div>
<div class="code">

<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">t'</span> <span class="id" title="var">T</span> <span class="id" title="var">HT</span> <span class="id" title="var">HE</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">HT</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;every&nbsp;case&nbsp;needs&nbsp;to&nbsp;introduce&nbsp;a&nbsp;couple&nbsp;of&nbsp;things&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t'</span> <span class="id" title="var">HE</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;and&nbsp;we&nbsp;can&nbsp;deal&nbsp;with&nbsp;several&nbsp;impossible<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;cases&nbsp;all&nbsp;at&nbsp;once&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span> <span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">HE</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_TESTTru&nbsp;*)</span> <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_TestFls&nbsp;*)</span> <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_Test&nbsp;*)</span> <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#T_Test"><span class="id" title="constructor">T_Test</span></a>; <span class="id" title="tactic">try</span> <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHHT1</span>; <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>
</div>

<div class="doc">
<font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab202"></a><h4 class="section">Exercise: 3 stars, advanced (finish_preservation_informal)</h4>
 Complete the following informal proof: 
<div class="paragraph"> </div>

 <i>Theorem</i>: If <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span>, then <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>. 
<div class="paragraph"> </div>

 <i>Proof</i>: By induction on a derivation of <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule in the derivation is <span class="inlinecode"><span class="id" title="var">T_Test</span></span>, then <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">test</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>
      <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>, with <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span>, <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>
      <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>.

<div class="paragraph"> </div>

      Inspecting the rules for the small-step reduction relation and
      remembering that <span class="inlinecode"><span class="id" title="var">t</span></span> has the form <span class="inlinecode"><span class="id" title="var">test</span></span> <span class="inlinecode">...</span>, we see that the
      only ones that could have been used to prove <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span> are
      <span class="inlinecode"><span class="id" title="var">ST_TestTru</span></span>, <span class="inlinecode"><span class="id" title="var">ST_TestFls</span></span>, or <span class="inlinecode"><span class="id" title="var">ST_Test</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the last rule was <span class="inlinecode"><span class="id" title="var">ST_TestTru</span></span>, then <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>.  But we
        know that <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, so we are done.

<div class="paragraph"> </div>


</li>
<li> If the last rule was <span class="inlinecode"><span class="id" title="var">ST_TestFls</span></span>, then <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>.  But we
        know that <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, so we are done.

<div class="paragraph"> </div>


</li>
<li> If the last rule was <span class="inlinecode"><span class="id" title="var">ST_Test</span></span>, then <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">test</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>
        <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span>, where <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span>.  We know <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span> so,
        by the IH, <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">Bool</span></span>.  The <span class="inlinecode"><span class="id" title="var">T_Test</span></span> rule then gives us
        <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">test</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>3</sub></span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, as required.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</li>
</ul>

</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_finish_preservation_informal" class="idref" href="#manual_grade_for_finish_preservation_informal"><span class="id" title="definition">manual_grade_for_finish_preservation_informal</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab203"></a><h4 class="section">Exercise: 3 stars, standard (preservation_alternate_proof)</h4>
 Now prove the same property again by induction on the
    <i>evaluation</i> derivation instead of on the typing derivation.
    Begin by carefully reading and thinking about the first few
    lines of the above proofs to make sure you understand what
    each one is doing.  The set-up for this proof is similar, but
    not exactly the same. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="preservation'" class="idref" href="#preservation'"><span class="id" title="lemma">preservation'</span></a> : <span class="id" title="keyword">∀</span> <a id="t:50" class="idref" href="#t:50"><span class="id" title="binder">t</span></a> <a id="t':51" class="idref" href="#t':51"><span class="id" title="binder">t'</span></a> <a id="T:52" class="idref" href="#T:52"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:50"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:52"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#t:50"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Types.html#t':51"><span class="id" title="variable">t'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t':51"><span class="id" title="variable">t'</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:52"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 The preservation theorem is often called <i>subject reduction</i>,
    because it tells us what happens when the "subject" of the typing
    relation is reduced.  This terminology comes from thinking of
    typing statements as sentences, where the term is the subject and
    the type is the predicate. 
</div>

<div class="doc">
<a id="lab204"></a><h2 class="section">Type Soundness</h2>

<div class="paragraph"> </div>

 Putting progress and preservation together, we see that a
    well-typed term can never reach a stuck state.  
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="multistep" class="idref" href="#multistep"><span class="id" title="definition">multistep</span></a> := (<a class="idref" href="Smallstep.html#multi"><span class="id" title="inductive">multi</span></a> <a class="idref" href="Types.html#step"><span class="id" title="inductive">step</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a id="a781e4b1e2c022f0326182a9bd099911" class="idref" href="#a781e4b1e2c022f0326182a9bd099911"><span class="id" title="notation">&quot;</span></a>t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span>' t<sub>2</sub>" := (<a class="idref" href="Types.html#multistep"><span class="id" title="definition">multistep</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Corollary</span> <a id="soundness" class="idref" href="#soundness"><span class="id" title="lemma">soundness</span></a> : <span class="id" title="keyword">∀</span> <a id="t:53" class="idref" href="#t:53"><span class="id" title="binder">t</span></a> <a id="t':54" class="idref" href="#t':54"><span class="id" title="binder">t'</span></a> <a id="T:55" class="idref" href="#T:55"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Types.html#t:53"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">\</span></a><a class="idref" href="Types.html#46525c5c9c73f3cc121f6ba0c58fa00e"><span class="id" title="notation">in</span></a> <a class="idref" href="Types.html#T:55"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Types.html#t:53"><span class="id" title="variable">t</span></a> <a class="idref" href="Types.html#a781e4b1e2c022f0326182a9bd099911"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Types.html#t':54"><span class="id" title="variable">t'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">~(</span></a><a class="idref" href="Types.html#stuck"><span class="id" title="definition">stuck</span></a> <a class="idref" href="Types.html#t':54"><span class="id" title="variable">t'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">t'</span> <span class="id" title="var">T</span> <span class="id" title="var">HT</span> <span class="id" title="var">P</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">P</span>; <span class="id" title="tactic">intros</span> [<span class="id" title="var">R</span> <span class="id" title="var">S</span>].<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#progress"><span class="id" title="axiom">progress</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">HT</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">HT</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">apply</span> <span class="id" title="var">IHP</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" title="tactic">apply</span> <a class="idref" href="Types.html#preservation"><span class="id" title="axiom">preservation</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">t</span> := <span class="id" title="var">x</span>); <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" title="tactic">unfold</span> <a class="idref" href="Types.html#stuck"><span class="id" title="definition">stuck</span></a>. <span class="id" title="tactic">split</span>; <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab205"></a><h2 class="section">Additional Exercises</h2>

<div class="paragraph"> </div>

<a id="lab206"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (subject_expansion)</h4>
 Having seen the subject reduction property, one might
    wonder whether the opposity property -- subject <i>expansion</i> --
    also holds.  That is, is it always the case that, if <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span>
    and <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, then <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>?  If so, prove it.  If
    not, give a counter-example.  (You do not need to prove your
    counter-example in Coq, but feel free to do so.)

<div class="paragraph"> </div>

    <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_subject_expansion" class="idref" href="#manual_grade_for_subject_expansion"><span class="id" title="definition">manual_grade_for_subject_expansion</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab207"></a><h4 class="section">Exercise: 2 stars, standard (variation1)</h4>
 Suppose that we add this new rule to the typing relation:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">T_SccBool</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">t</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" title="var">t</span> \<span class="id" title="tactic">in</span> <span class="id" title="var">Bool</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" title="var">scc</span> <span class="id" title="var">t</span> \<span class="id" title="tactic">in</span> <span class="id" title="var">Bool</span>
<div class="paragraph"> </div>

</span>   Which of the following properties remain true in the presence of
   this rule?  For each one, write either "remains true" or
   else "becomes false." If a property becomes false, give a
   counterexample.
<ul class="doclist">
<li> Determinism of <span class="inlinecode"><span class="id" title="var">step</span></span>
            <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</li>
<li> Progress
            <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</li>
<li> Preservation
            <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</li>
</ul>

</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_variation1" class="idref" href="#manual_grade_for_variation1"><span class="id" title="definition">manual_grade_for_variation1</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab208"></a><h4 class="section">Exercise: 2 stars, standard (variation2)</h4>
 Suppose, instead, that we add this new rule to the <span class="inlinecode"><span class="id" title="var">step</span></span> relation:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">ST_Funny1</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">test</span> <span class="id" title="var">tru</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">t<sub>3</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" title="var">t<sub>3</sub></span>
<div class="paragraph"> </div>

</span>   Which of the above properties become false in the presence of
   this rule?  For each one that does, give a counter-example.
            <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_variation2" class="idref" href="#manual_grade_for_variation2"><span class="id" title="definition">manual_grade_for_variation2</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab209"></a><h4 class="section">Exercise: 2 stars, standard, optional (variation3)</h4>
 Suppose instead that we add this rule:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">ST_Funny2</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">t<sub>2</sub>'</span> <span class="id" title="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t<sub>2</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" title="var">t<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">test</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">t<sub>3</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" title="var">test</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub>'</span> <span class="id" title="var">t<sub>3</sub></span>)
<div class="paragraph"> </div>

</span>   Which of the above properties become false in the presence of
   this rule?  For each one that does, give a counter-example.
            <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab210"></a><h4 class="section">Exercise: 2 stars, standard, optional (variation4)</h4>
 Suppose instead that we add this rule:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">ST_Funny3</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">prd</span> <span class="id" title="var">fls</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" title="var">prd</span> (<span class="id" title="var">prd</span> <span class="id" title="var">fls</span>))
<div class="paragraph"> </div>

</span>   Which of the above properties become false in the presence of
   this rule?  For each one that does, give a counter-example.
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab211"></a><h4 class="section">Exercise: 2 stars, standard, optional (variation5)</h4>
 Suppose instead that we add this rule:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">T_Funny4</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" title="var">zro</span> \<span class="id" title="tactic">in</span> <span class="id" title="var">Bool</span>
<div class="paragraph"> </div>

</span>   Which of the above properties become false in the presence of
   this rule?  For each one that does, give a counter-example.
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab212"></a><h4 class="section">Exercise: 2 stars, standard, optional (variation6)</h4>
 Suppose instead that we add this rule:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">T_Funny5</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" title="var">prd</span> <span class="id" title="var">zro</span> \<span class="id" title="tactic">in</span> <span class="id" title="var">Bool</span>
<div class="paragraph"> </div>

</span>   Which of the above properties become false in the presence of
   this rule?  For each one that does, give a counter-example.
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

<a id="lab213"></a><h4 class="section">Exercise: 3 stars, standard, optional (more_variations)</h4>
 Make up some exercises of your own along the same lines as
    the ones above.  Try to find ways of selectively breaking
    properties -- i.e., ways of changing the definitions that
    break just one of the properties and leave the others alone.

</div>
<div class="code">
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab214"></a><h4 class="section">Exercise: 1 star, standard (remove_prdzro)</h4>
 The reduction rule <span class="inlinecode"><span class="id" title="var">ST_PrdZro</span></span> is a bit counter-intuitive: we
    might feel that it makes more sense for the predecessor of <span class="inlinecode"><span class="id" title="var">zro</span></span> to
    be undefined, rather than being defined to be <span class="inlinecode"><span class="id" title="var">zro</span></span>.  Can we
    achieve this simply by removing the rule from the definition of
    <span class="inlinecode"><span class="id" title="var">step</span></span>?  Would doing so create any problems elsewhere?

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_remove_predzro" class="idref" href="#manual_grade_for_remove_predzro"><span class="id" title="definition">manual_grade_for_remove_predzro</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab215"></a><h4 class="section">Exercise: 4 stars, advanced (prog_pres_bigstep)</h4>
 Suppose our evaluation relation is defined in the big-step style.
    State appropriate analogs of the progress and preservation
    properties. (You do not need to prove them.)

<div class="paragraph"> </div>

    Can you see any limitations of either of your properties?  Do they
    allow for nonterminating commands?  Why might we prefer the
    small-step semantics for stating preservation and progress?

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>

</div>
<div class="code">
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_prog_pres_bigstep" class="idref" href="#manual_grade_for_prog_pres_bigstep"><span class="id" title="definition">manual_grade_for_prog_pres_bigstep</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<br/>
<span class="comment">(*&nbsp;2020-08-24&nbsp;16:13&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>